package no.uio.ifi.cop.prover;


import java.util.Map;
import java.util.HashMap;
import java.util.LinkedHashMap;

import no.uio.ifi.cop.common.Global;
import no.uio.ifi.cop.cl.Predicate;

import no.uio.ifi.cop.prover.factorder.RandomMap;
import no.uio.ifi.cop.prover.factorder.IgnoreMap;

/**
 * Stores a set of predicates for a single branch
 * in a proof tree.
 *
 * @version 1.0
 * @author  bjarneh@ifi.uio.no
 */

public final class FactSet implements Cloneable{

    private Map<String, Predicate> matched;
    private Map<String, Predicate> unmatched;

    public FactSet(){

        if( Global.getBool("-ignore") ) {
            matched = new IgnoreMap<String, Predicate>();
        }else{
            matched = new HashMap<String, Predicate>(200);
        }

        if( Global.get("-order").equals("random") ){
            unmatched = new RandomMap<String, Predicate>();
        }else if( Global.get("-order").equals("time") ){
            unmatched = new LinkedHashMap<String, Predicate>();
        }else{
            unmatched = new HashMap<String, Predicate>();
        }
    }

    // never add a predicate which is alredy matched
    public void add(Predicate t){
        if(! contains( t ) ){
            unmatched.put(t.toString(), t);
        }
    }

    public boolean contains(Predicate t){
        Predicate p = matched.get(t.toString());
        return p != null;
    }

    // unmatched => matched
    public void update(){
        for(String k: unmatched.keySet()){
            matched.put(k, unmatched.get(k));
        }
        unmatched.clear();
    }

    public Predicate getSingle(){
        if( ! hasNewFacts() ){ return null;  }
        // ugly...
        for(Predicate p: unmatched.values()){ return p; }
        return null;
    }

    public void updateSingle(Predicate t){
        // actually fails to prove yablo.gl when used facts are inserted
        // into the matched set again.. a bug leads to proof :-)
        matched.put(t.toString(), unmatched.get(t.toString()));
        unmatched.remove(t.toString());
    }

    public boolean hasNewFacts(){
        return unmatched.size() > 0;
    }

    public Iterable<Predicate> iterMatched(){
        return matched.values();
    }

    public Iterable<Predicate> iterUnmatched(){
        return unmatched.values();
    }

    // dot-graph messes up successful random order
    public Iterable<Predicate> iterUnshuffled(){
        if( unmatched instanceof RandomMap ){
            return ((RandomMap<String, Predicate>) unmatched).unshuffled();
        }else{
            return iterUnmatched();
        }
    }

    // make shallow clone
    public FactSet clone(){

        FactSet fresh = new FactSet();

        for(String k: matched.keySet()){
            fresh.matched.put(k, matched.get(k));
        }
        for(String k: unmatched.keySet()){
            fresh.unmatched.put(k, unmatched.get(k));
        }
        return fresh;
    }

    public String toString(){

        StringBuilder sb = new StringBuilder();

        sb.append("[FactSet]\n------old-----\n");

        for(String k: matched.keySet()){
            sb.append(k+ " ");
        }

        if( unmatched.size() > 0){
            sb.append("\n------new-----\n");
            for(String k: unmatched.keySet()){
                sb.append(k+ " ");
            }
        }
        return sb.toString();
    }
}
